// Javascript internationalisation
ENUM["section"]="Sections";
ENUM["reference"]="References";
ENUM["glossary"]="Glossary";